//------------------------------------------------------------------------------
// The confidential and proprietary information contained in this file may
// only be used by a person authorised under and to the extent permitted
// by a subsisting licensing agreement from ARM Limited.
//
//            (C) COPYRIGHT 2004-2010 ARM Limited.
//                ALL RIGHTS RESERVED
//
// This entire notice must be reproduced on all copies of this file
// and copies of this file may only be made by a person if such person is
// permitted to do so under the terms of a subsisting license agreement
// from ARM Limited.
//
//      SVN Information
//
//      Checked In          :  2010-10-06 05:43:00 +0100 (Wed, 06 Oct 2010)
//
//      Revision            : 96704
//
//      Release Information :
//
//------------------------------------------------------------------------------

//------------------------------------------------------------------------------
//  Purpose : AMBA3 Peripheral Bus Protocol checker (APB PC) using OVLs
//             - Supports address bus widths up to 32-bit
//             - Supports data bus widths up to 32-bit
//             - Supports optional port PCLKEN
//             - Supports optional port PREADY (slave)
//             - Supports optional port PSLVERR (slave)
//------------------------------------------------------------------------------

//------------------------------------------------------------------------------
// Module Declaration
//------------------------------------------------------------------------------

module ApbPC (
    // Global Signals
    PCLK,
    PCLKEN,
    PRESETn,

    // APB Control Signals
    PSELx,
    PENABLE,
    PWRITE,
    PREADY,
    PSLVERR,

    // APB Data Signals
    PADDR,
    PWDATA,
    PRDATA
  );

//------------------------------------------------------------------------------
// Parameters Declaration
//------------------------------------------------------------------------------

  // Configurable (user can set)
  // =====
  // Parameters below can be set by the user.

  // Set ADDR_WIDTH to the PADDR bus width required
  parameter ADDR_WIDTH = 32;
  // Set DATA_WIDTH to the P*DATA buses width required
  parameter DATA_WIDTH = 32;
  // Set SEL_WIDTH to the PSELx bus width required
  parameter SEL_WIDTH  = 1;

  // OVL instances property_type parameter (0=assert, 1=assume, 2=ignore)
  parameter APB_ERRM_PropertyType    = 0; // default: assert, Master is APB compliant
  parameter APB_ERRS_PropertyType    = 0; // default: assert, Slave is APB compliant
  parameter APB_ERRP_PropertyType    = 0; // default: assert, Parameters are APB compliant

  // Optional signals parameter (0=not present, 1=present)
  parameter APB_PCLKEN_Present       = 1; // default: optional PCLKEN signal is present
  parameter APB_PREADY_Present       = 1; // default: optional PREADY signal is present
  parameter APB_PSLVERR_Present      = 1; // default: optional PSLVERR signal is present


  // Calculated (user should not override)
  // =====
  // Do not override the following parameters: they must be calculated exactly
  // as shown below

  // Resolving property type priority for PREADY checks which can be either
  // PREADY_PropertyType or ERRS_PropertyType
  parameter APB_ERR_PREADY_PropertyType   =
    (APB_PREADY_Present == 1) ? APB_ERRS_PropertyType : 2;

  // Resolving property type priority for PSLVERR checks which can be either
  // PSLVERR_PropertyType or ERRS_PropertyType
  parameter APB_ERR_PSLVERR_PropertyType  =
    (APB_PSLVERR_Present == 1) ? APB_ERRS_PropertyType : 2;

  // Max indexes
  parameter DATA_MAX = DATA_WIDTH - 1; 
  parameter ADDR_MAX = ADDR_WIDTH - 1;
  parameter SEL_MAX  = SEL_WIDTH - 1;

//------------------------------------------------------------------------------
// Inputs Declaration (no outputs)
//------------------------------------------------------------------------------

  // Global Signals
  // =====
  input               PCLK;
  input               PCLKEN;
  input               PRESETn;

  // APB Control Signals
  // =====
  input [SEL_MAX:0]   PSELx;
  input               PENABLE;
  input               PWRITE;
  input               PREADY;
  input               PSLVERR;

  // APB Data Signals
  // =====
  input [ADDR_MAX:0]  PADDR;
  input [DATA_MAX:0]  PWDATA;
  input [DATA_MAX:0]  PRDATA;


//------------------------------------------------------------------------------
// Wire and Reg Declarations
//------------------------------------------------------------------------------

  // APB control signals
  wire [SEL_MAX:0]    PSELx;
  wire                PENABLE;
  wire                PWRITE;
  wire                PSELall;
  wire                StartTrans;
  wire                EndTrans;
  wire                InTrans;

  // Registered APB control signals
  reg [SEL_MAX:0]     PSELreg;
  reg                 PENABLEreg;
  reg                 PREADYreg;
  reg                 PSLVERRreg;
  reg                 PWRITEreg;
  reg                 InTransreg;
  reg                 StartTransreg;
  reg                 EndTransreg;

  // APB data signals
  wire  [ADDR_MAX:0]  PADDR;
  wire  [DATA_MAX:0]  PWDATA;
  wire  [DATA_MAX:0]  PRDATA;

  // Registered APB control signals
  reg   [ADDR_MAX:0]  PADDRreg;
  reg   [DATA_MAX:0]  PWDATAreg;
  reg   [DATA_MAX:0]  PRDATAreg;

  // Optional signals
  wire                PCLKENopt;
  wire                PREADYopt;
  wire                PSLVERRopt;

//------------------------------------------------------------------------------
// Optional Signal Assignment
//------------------------------------------------------------------------------
  assign PCLKENopt  = (APB_PCLKEN_Present  == 1) ? PCLKEN  : 1'b1;
  assign PREADYopt  = (APB_PREADY_Present  == 1) ? PREADY  : 1'b1;
  assign PSLVERRopt = (APB_PSLVERR_Present == 1) ? PSLVERR : 1'b0;

//------------------------------------------------------------------------------
// Defines Declaration
//------------------------------------------------------------------------------

  // Clock and Reset
  // =====
  // Can be overridden by user
  //
  `ifdef APB_OVL_CLK
  `else
     `define APB_OVL_CLK PCLK
  `endif
  //
  `ifdef APB_OVL_RSTn
  `else
     `define APB_OVL_RSTn PRESETn
  `endif
  //
  // OVL Version Specific Macros
  `ifdef APB_USE_OLD_OVL
     // Old OVL library from April 2003
     // ===============================
     // severity_level
     `define APB_SimFatal   0
     `define APB_SimError   1
     `define APB_SimWarning 2
  `else
     // Accellera V1.0 and later
     // ========================
     `include "std_ovl_defines.h"
     // severity_level
     `define APB_SimFatal   `OVL_FATAL
     `define APB_SimError   `OVL_ERROR
     `define APB_SimWarning `OVL_WARNING
     //
     // Disable for X-checking
     `ifdef     OVL_XCHECK_OFF
        `define APB_XCHECK_OFF
     `endif
   `endif

//------------------------------------------------------------------------------
// Initialize simulation 
//------------------------------------------------------------------------------

  initial
  begin
    // Format for time reporting
    // =====
    // Format for time reporting
    $timeformat(-9, 0, " ns", 0);

    // Indicate version and release state of ApbPC
    // =====
    $display("APB_INFO: Running ApbPC release PL401-r0p1-00eac0             ");

    // Warn if any/some channel rules are ignored
    // =====
    if (APB_ERRM_PropertyType == 2)        $display("APB_WARN: All APB_ERRM_* rules have been ignored by the APB_ERRM_PropertyType parameter");
    if (APB_ERRS_PropertyType == 2)        $display("APB_WARN: All APB_ERRS_* rules have been ignored by the APB_ERRS_PropertyType parameter");
    if (APB_ERR_PREADY_PropertyType == 2)  $display("APB_WARN: All APB_ERR_PREADY_* rules have been ignored by the APB_ERR_PREADY_PropertyType parameter");
    if (APB_ERR_PSLVERR_PropertyType == 2) $display("APB_WARN: All APB_ERR_PSLVERR_* rules have been ignored by the APB_ERR_PSLVERR_PropertyType parameter");
  end

  // All registers are gated by PCLKENopt
  always @ (posedge `APB_OVL_CLK or negedge `APB_OVL_RSTn)
  begin
    if  (~`APB_OVL_RSTn)
    begin
      PSELreg       <= {SEL_WIDTH{1'b0}};
      PENABLEreg    <= 1'b0;
      PWRITEreg     <= 1'b0;
      PREADYreg     <= 1'b0;
      PSLVERRreg    <= 1'b0;
      PADDRreg      <= {ADDR_WIDTH{1'b0}};
      PWDATAreg     <= {DATA_WIDTH{1'b0}};
      PRDATAreg     <= {DATA_WIDTH{1'b0}};
      InTransreg    <= 1'b0;
      StartTransreg <= 1'b0;
      EndTransreg   <= 1'b0;
    end
    else if (PCLKENopt)
    begin
      PSELreg       <= PSELx;
      PENABLEreg    <= PENABLE;
      PWRITEreg     <= PWRITE;
      PREADYreg     <= PREADYopt;
      PSLVERRreg    <= PSLVERRopt;
      PADDRreg      <= PADDR;
      PWDATAreg     <= PWDATA;
      PRDATAreg     <= PRDATA;
      InTransreg    <= InTrans;
      StartTransreg <= StartTrans;
      EndTransreg   <= EndTrans;
    end
  end

  // OR-reduce PSELx
  assign PSELall = PCLKENopt & (|PSELx);

  // APB transfer
  assign StartTrans = PSELall & ~PENABLE;
  assign EndTrans   = PSELall &  PENABLE & PREADYopt;
  assign InTrans    = InTransreg ? ~EndTrans : StartTrans;

//------------------------------------------------------------------------------
// Parameters Rules
//------------------------------------------------------------------------------

  // APB_ERRP_DATAWIDTH
  // =====
  assert_never #(`APB_SimFatal, APB_ERRP_PropertyType,
    "APB_ERRP_DATAWIDTH. DATA_WIDTH value greater than 32 is not permitted."
  ) u_pxdata_width
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr ((DATA_WIDTH > 32))
     );

  // APB_ERRP_ADDRWIDTH
  // =====
  assert_never #(`APB_SimFatal, APB_ERRP_PropertyType,
    "APB_ERRP_ADDRWIDTH. ADDR_WIDTH value greater than 32 is not permitted."
  ) u_paddr_width
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr ((ADDR_WIDTH > 32))
     );

//------------------------------------------------------------------------------
// APB Transfer
//------------------------------------------------------------------------------

  // APB_ERRM_PSEL_1HOT
  // =====
  // NB: extended PSELx by 1-bit (set to zero) to avoid warning when SEL_WIDTH=1
  assert_zero_one_hot #(`APB_SimError, (SEL_WIDTH+1), APB_ERRM_PropertyType,
    "APB_ERRM_PSEL_1HOT. When not in reset, PSELx must be zero or one-hot encoded."
  ) u_psel_1hot
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr ({SEL_WIDTH+1{PCLKENopt}} & {1'b0, PSELx})
     );

  // APB_ERRM_PSEL_2CYCLE
  // =====
  //Check PSELx doesn't go high for 2 cycles without PENABLE going high
  assert_never #(`APB_SimError, APB_ERRM_PropertyType,
    "APB_ERRM_PSEL_2CYCLE. When not in reset, PSELx asserted for 2 cycles without PENABLE high is not permitted."
  ) u_psel_2cycle
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (StartTransreg & StartTrans)
     );

  // APB_ERRM_PSEL_CHG
  // =====
  assert_never #(`APB_SimError, APB_ERRM_PropertyType,
    "APB_ERRM_PSEL_CHG. During an APB transaction, PSELx value change is not permitted."
  ) u_psel_chg
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (InTransreg & |(PSELx ^ PSELreg))
    );

  // APB_ERRM_PSEL_PENABLE
  // =====
  assert_never #(`APB_SimError, APB_ERRM_PropertyType,
    "APB_ERRM_PSEL_PENABLE. At the start of an APB transaction, PSELx and PENABLE both high is not permitted."
  ) u_psel_penable
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (PSELall & PENABLE & (~(|PSELreg) | EndTransreg))
     );

  // APB_ERRM_PENABLE_LOW
  // =====
  assert_never #(`APB_SimError, APB_ERRM_PropertyType,
    "APB_ERRM_PENABLE_LOW. During an APB transaction, PENABLE deasserted is not permitted."
  ) u_penable_low
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (InTransreg & ~PENABLE)
     );

  // APB_ERRM_PADDR_CHG
  // =====
  assert_never #(`APB_SimError, APB_ERRM_PropertyType,
    "APB_ERRM_PADDR_CHG. During an APB transaction, PADDR value change is not permitted."
  ) u_paddr_chg
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (InTransreg & |(PADDR ^ PADDRreg))
     );

  // APB_ERRM_PADDR_LSB_CHECK
  // =====
  assert_always #(`APB_SimWarning, APB_ERRM_PropertyType ,
    "APB_ERRM_PADDR_LSB_CHECK.  At the start of an APB transaction, PADDR[1:0] should be zero."
  ) u_paddr_lsb_chk
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (StartTrans & (PADDR[1:0] == 2'b00))
     );

  // APB_ERRM_PWRITE_CHG
  // =====
  assert_never #(`APB_SimError, APB_ERRM_PropertyType,
    "APB_ERRM_PWRITE_CHG. During an APB transaction, PWRITE value change is not permitted."
  ) u_pwrite_chg
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (InTransreg & (PWRITE ^ PWRITEreg))
     );

  // APB_ERRM_PWDATA_CHG
  // =====
  assert_never #(`APB_SimError, APB_ERRM_PropertyType,
    "APB_ERRM_PWDATA_CHG. During an APB transaction, PWDATA value change is not permitted"
  ) u_pwdata_chg
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (InTransreg & PWRITE & |(PWDATA ^ PWDATAreg))
     );

  // APB_ERRM_PENABLE_HIGH
  // =====
  assert_never #(`APB_SimError, APB_ERRM_PropertyType,
  "APB_ERRM_PENABLE_HIGH. At the end of an APB transaction, PENABLE staying high is not permitted"
  ) u_penable_high
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (PENABLE & EndTransreg)
     );

//------------------------------------------------------------------------------
// APB Reset State
//------------------------------------------------------------------------------

  // APB_ERRM_RST_PSEL
  // =====
  assert_never #(`APB_SimError, APB_ERRM_PropertyType,
    "APB_ERRM_RST_PSEL. When in reset, value other than 0 on PSELx is not permitted."
  ) u_psel_reset
    (.clk       (`APB_OVL_CLK),
     .reset_n   (~`APB_OVL_RSTn),
     .test_expr (PSELall)
     );

//------------------------------------------------------------------------------
// X-Propagation Rules
//------------------------------------------------------------------------------
`ifdef APB_XCHECK_OFF
`else  // X-Checking on by default

  // APB_ERRM_PSEL_X
  // =====
  assert_never_unknown #(`APB_SimError, SEL_WIDTH, APB_ERRM_PropertyType,
    "APB_ERRM_PSEL_X. When not in reset, a value of X on PSELx is not permitted."
  ) u_psel_xcheck
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .qualifier (PCLKENopt),
     .test_expr (PSELx)
     );

  // APB_ERRM_PENABLE_X
  // =====
  assert_never_unknown #(`APB_SimError, 1, APB_ERRM_PropertyType,
    "APB_ERRM_PENABLE_X. When not in reset, a value of X on PENABLE is not permitted."
  ) u_penable_xcheck
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .qualifier (PCLKENopt),
     .test_expr (PENABLE)
     );

  // APB_ERRM_PWRITE_X
  // =====
  assert_never_unknown #(`APB_SimError, 1, APB_ERRM_PropertyType,
    "APB_ERRM_PWRITE_X. When PSELx is high, a value of X on PWRITE is not permitted."
  ) u_pwrite_xcheck
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .qualifier (PSELall),
     .test_expr (PWRITE)
     );

  // APB_ERRM_PADDR_X
  // =====
  assert_never_unknown #(`APB_SimError, ADDR_WIDTH, APB_ERRM_PropertyType,
    "APB_ERRM_PADDR_X. When PSELx is high, a value of X on PADDR is not permitted."
  ) u_paddr_xcheck
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .qualifier (PSELall),
     .test_expr (PADDR)
     );

  // APB_ERRM_PWDATA_X
  // =====
  assert_never_unknown #(`APB_SimError, DATA_WIDTH, APB_ERRM_PropertyType,
    "APB_ERRM_PWDATA_X. When PSELx and PWRITE are high, a value of X on PWDATA is not permitted."
  ) u_pwdata_xcheck
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .qualifier (PSELall & PWRITE),
     .test_expr (PWDATA)
     );

  // APB_ERR_PREADY_X
  // =====
  assert_never_unknown #(`APB_SimError, 1, APB_ERR_PREADY_PropertyType,
    "APB_ERR_PREADY_X. When PSELx and PENABLE are high, a value of X on PREADY is not permitted."
  ) u_pready_xcheck
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .qualifier (PSELall & PENABLE),
     .test_expr (PREADYopt)
     );

  // APB_ERR_PSLVERR_X
  // =====
  assert_never_unknown #(`APB_SimError, 1, APB_ERR_PSLVERR_PropertyType,
    "APB_ERR_PSLVERR_X. When PSELx, PENABLE and PREADY are high, a value of X on PSLVERR is not permitted."
  ) u_pslverr_xcheck
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .qualifier (EndTrans),
     .test_expr (PSLVERRopt)
     );

  // APB_ERRS_PRDATA_X
  // =====
  assert_never_unknown #(`APB_SimError, DATA_WIDTH, APB_ERRS_PropertyType,
    "APB_ERRS_PRDATA_X. When PSELx, PENABLE, PREADY are high and PWRITE is low, a value of X on PRDATA is not permitted."
  ) u_prdata_xcheck
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .qualifier (PSELall & PENABLE & ~PWRITE & PREADYopt),
     .test_expr (PRDATA)
     );

`endif //APB_XCHECK_OFF

//------------------------------------------------------------------------------
// Power Efficiency
//------------------------------------------------------------------------------

  // APB_ERRM_PADDR_STABLE
  // =====
  assert_never #(`APB_SimWarning, APB_ERRM_PropertyType,
    "APB_ERRM_PADDR_STABLE. PADDR should only change at the start or after a transaction."
  ) u_paddr_stable
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (~StartTrans & ~EndTransreg & |(PADDR ^ PADDRreg))
     );

  // APB_ERRM_PWDATA_STABLE
  // =====
  assert_never #(`APB_SimWarning, APB_ERRM_PropertyType,
    "APB_ERRM_PWDATA_STABLE. PWDATA should only change at the start of a transaction."
  ) u_pwdata_stable
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (~StartTrans & |(PWDATA ^ PWDATAreg))
     );

  // APB_ERRM_PWRITE_STABLE
  // =====
  assert_never #(`APB_SimWarning, APB_ERRM_PropertyType,
    "APB_ERRM_PWRITE_STABLE. PWRITE should only change at the start or after a transaction."
  ) u_pwrite_stable
    (.clk       (`APB_OVL_CLK),
     .reset_n   (`APB_OVL_RSTn),
     .test_expr (~StartTrans & ~EndTransreg & (PWRITE ^ PWRITEreg))
     );

//------------------------------------------------------------------------------
// Undefines Declaration
//------------------------------------------------------------------------------

  // Clock and Reset
  // =====
  `undef APB_OVL_CLK
  `undef APB_OVL_RSTn

  // OVL Severity levels
  // =====
  `undef APB_SimFatal
  `undef APB_SimError
  `undef APB_SimWarning

  // Others
  // =====
  `ifdef APB_USE_OLD_OVL
  `else
    `ifdef OVL_XCHECK_OFF
      `undef APB_XCHECK_OFF
    `endif
  `endif

//------------------------------------------------------------------------------
// End of Module
//------------------------------------------------------------------------------

endmodule //ApbPC

